A:Type, eq:EqDecider(A), B:(AType), g:x:A fp B(x), x:A.
x  dom(g)  fpf-normalize(eq;g)(x) = g(x)  B(x) 

latex

Definitions

f(x), x  dom(f), f(x)?z, , f  g, x : v, fpf-normalize(eq;g), x:AB(x), a:A fp B(a), Type, t  T, x:A. B(x), EqDecider(T), x:AB(x), f(a), x(s), x. t(x), x.A(x), Top, b, P  Q, , false, eqof(d), p  q, if b t else f fi, reduce(f;k;as), nil, <a,b>, 2of(t), 1of(t), b, filter(P;l), car.cdr, s ~ t, Void, x:A. B(x), s = t, (x  l), {x:A| B(x) }, type List, False, deq-member(eq;x;L), , A, Prop, P & Q, P  Q, Unit, left+right, S  T, P  Q, {T}, P  Q

Lemmas

cons member, subtype rel self, implies functionality wrt iff, assert-deq-member, deq property, deq-member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, eqof wf, bool wf, false wf, list-subtype, l member wf, top wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, deq wf